Nuprl Lemma : trigger1-p_wf
11,40
postcript
pdf
T
,
A
:Type,
P
:(
A
T
),
i
:Id,
k
:Knd,
a
,
x
:Id,
es
:ES.
@
i
k
(v:
T
) triggers local action
a
when
P
(
x
:
A
) v
latex
Definitions
x
.
t
(
x
)
,
A
c
B
,
e
@
i
.
P
(
e
)
,
(
e
<loc
e'
)
,
x
:
A
.
B
(
x
)
,
P
Q
,
P
&
Q
,
@
i
k
(v:
T
) triggers local action
a
when
P
(
x
:
A
) v
,
,
t
T
,
Knd
,
x
:
A
.
B
(
x
)
,
P
Q
,
x
(
s
)
,
e
@
i
.
P
(
e
)
Lemmas
bool
wf
,
IdLnk
wf
,
event
system
wf
,
locl
wf
,
es-kind
wf
,
es-val
wf
,
es-vartype
wf
,
es-locl-iff
,
es-loc-pred
,
es-when
wf
,
assert
wf
,
es-causl
wf
,
es-loc
wf
,
Id
wf
,
alle-at
wf
origin
T, A:Type, P:(A
T
), i:Id, k:Knd, a, x:Id, es:ES.
T, A:Type, P:(AT), i:Id, k:Knd, a, x:Id, es:ES.
x. t(x)
B
e@i.P(e)x:A. B(x)
Q Tx:A. B(x)
Qe@i. P(e)